from z3 import *

S = DeclareSort("S")
# f 是一个一元函数
f = Function("f", S, S)
# x 是一个常数
x = Const("x", S)
solve(f(f(x)) == x, f(f(f(x))) == x)
# > [x = S!val!0, f = [else -> S!val!0]]

solve(f(f(x)) == x, f(f(f(x))) == x, f(x) != x)
# > no solution
